This is going go make a lot of unfolds useless. At the meeting we decided to also make a PR to warn on unfolds that don't do anything.

Good from the proof maintenance side.

@strub are we good on code style? (I'd like @oskgo to merge on June 1st so I can issue the pre-release after the breaking change, but also not too late.)

Note

I also ran across a bug where declarations such as def foo (x y: int) / = true auto-unfolded after being given only one argument rather than requiring two. This PR fixes that as well. The fix is a one-liner, so it shouldn't be necessary to split up the PR IMO.

I say we fold the proof fixes into the main commit, but keep this little one separate and in this PR.

This is going go make a lot of unfolds useless. At the meeting we decided to also make a PR to warn on unfolds that don't do anything.

I guess this would also include warning about unfolds of non-existent operators. I've always found it weird that this isn't flagged.

A quick note on the SPHINCS+ external CI check. At present, this checks because there is a nicely-named branch there. But the (local) CI for that nicely-named branch fails currently, because the remote repo has been stabilised by @MM45 as part of his dissertation artefact.

Two options:

1. We take over Matthias's personal repo (after understanding stability constraints); or
2. We fork it as formosa-crypto/formosa-slhdsa and move external CI to that.

This affects merging here: if we merge this, we currently have no way of making sure that CI doesn't fail on main without breaking the local CI on the external repo.

@alleystoughton I found out that there's an existing pragma enabling those warnings. I don't know why it isn't enabled by default.

@fdupress In terms of the external SPHINCS+ CI, I think either option works (the CI on that repo can simply be updated to always use the most recent EC instead of a fixed version, as the actual dissertation artifact is in a separate repostory). I suppose, however, that we would eventually want to move it to formosa anyways, so we might as well do that now?

Thanks, @MM45 .

I've created the formosa-crypto/formosa-slhdsa repo and the old CI is running now. Once that succeeds, I'll point the external CI job there and we can rebase this.

I've removed the CI cleanup commits instead of stacking extra commits removing them, so it's not a clean fork. Keep that in mind if you want to backport changes to your copy. (I would suggest doing so only on EC releases—you can just bump the EasyCrypt version in your docker container, and cherry-pick the fixes across to your branch.)